Nuprl Definition : Q-R-glues
11,40
postcript
pdf
g
glues
Ia
:
Qa
f
Ib
:
Rb
== {
Ia
}
=
g
== {
Ib
} &
g
is
Qa
-
Rb
-pre-preserving on {
Ib
}
==
& Inj({
e
:E|
(
e
Ib
)} ;E;
g
)
==
& (
e
:E(
Ib
).
f
(
g
(
e
)) =
Ib
(
e
))
latex
clarification:
Q-R-glues(
es
;
Ib_valtype
;
g
;
f
;
Ia
;
Qa
;
Ib
;
Rb
)
== weak-antecedent-surjection(
es
;{
Ib
};{
Ia
};
g
) & Q-R-pre-preserving(
es
;
g
;{
Ib
};
Qa
;
Rb
)
==
& Inj({
e
:es-E(
es
)|
(
e
Ib
)} ;es-E(
es
);
g
)
==
& (
e
:es-E-interface(
es
;
Ib
).
f
(
g
(
e
)) =
Ib
(
e
)
Ib_valtype
)
latex
Definitions
Q
=
f
==
P
,
f
is
Q
-
R
-pre-preserving on
P
,
{
I
}
,
P
&
Q
,
Inj(
A
;
B
;
f
)
,
{
x
:
A
|
B
(
x
)}
,
b
,
e
X
,
E
,
x
:
A
.
B
(
x
)
,
E(
X
)
,
s
=
t
,
f
(
a
)
,
X
(
e
)
FDL editor aliases
Q-R-glues
origin